$\forall$$T$:Type, ${\it LL}$:($T$ List) List. concat(${\it LL}$) $=$ nil $\in$ $T$ List $\Leftrightarrow$ ($\forall$$L$$\in$${\it LL}$. $L$ $=$ nil $\in$ $T$ List)